ds:x:Id fp Type, da:k:Knd fp Type, v:ecl-trans-tuple{i:l}(ds;da), L:event-info(ds;da) List, m:.
ecl-trans-normal(v)
 (L1:event-info(ds;da) List. L1  L  ecl-trans-halt2(ds;da;v)(0,L1)  False)
 (ecl-trans-act(ds;da;v)(m,L)  ecl-trans-act(ds;da;reset-ecl-tuple(v))(m,L)) 

latex

Definitions

Id, t  T, x. t(x), x:A. B(x), a:A fp B(a), Knd, ecl-trans-tuple{i:l}(ds;da), event-info(ds;da), , ecl-trans-normal(x), AB, P  Q, False, A, Prop, ecl-trans-halt2(ds;da;A), l1  l2, reset-ecl-tuple(A), ecl-trans-act(ds;da;A), P  Q, P & Q, P  Q, P  Q, Dec(P), null(as), b, x:A. B(x), let x,y,z = a in t(x;y;z), IdLnkDeq, sum-deq(A;B;a;b), sumdeq(a;b), union-deq(A;B;a;b), KindDeq, Top, i=j, NatDeq, atom-deq-aux, x=yAtom, AtomDeq, prod-deq(A;B;a;b), p  q, proddeq(a;b), product-deq(A;B;a;b), IdDeq, 2of(t), f(x), 1of(t), eqof(d), p  q, reduce(f;k;as), deq-member(eq;x;L), x  dom(f), f(x)?z, State(ds), IdLnk, tl(l), i<j, b, ij, if b t else f fi, nth_tl(n;as), hd(l), l[i], Y, ||as||, (x  l), last(L), as @ bs, ij, {T}, SQType(T), let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), Valtype(da;k), S  T, , , ecl-trans-type(A), ecl-trans-state(v;L), Unit, A & B, x,y. t(x;y), ecl-trans-state-from(v;z;L), ecl-trans-init(v), ecl-trans-h(v)

Lemmas

ecl-trans-act-functionality2, list accum append, not functionality wrt iff, assert-deq-member, deq-member wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf, ecl-trans-state wf, l member wf, ma-valtype wf, bool wf, nat plus wf, subtype rel self, decl-state wf, fpf-cap wf, Kind-deq wf, top wf, append wf, ecl-trans-act functionality, iseg length, length append, iseg transitivity, cons one one, non neg length, length wf1, member wf, iseg append0, last wf, last lemma, decidable false, append is nil, assert of null, decidable assert, null wf, ecl-trans-act wf, reset-ecl-tuple wf, iseg wf, ecl-trans-halt2 wf, false wf, le wf, ecl-trans-normal wf, nat wf, event-info wf, ecl-trans-tuple wf, Knd wf, fpf wf, Id wf